{ compiling RepeatedCase._+_
RepeatedCase._+_ =
  λ a b →
    case a of
      RepeatedCase.N.zero → b
      RepeatedCase.N.suc c → RepeatedCase.N.suc (RepeatedCase._+_ c b)
}
{ compiling RepeatedCase.P.fst
RepeatedCase.P.fst = λ a → case a of RepeatedCase._,_ b _ → b
}
{ compiling RepeatedCase.P.snd
RepeatedCase.P.snd = λ a → case a of RepeatedCase._,_ _ b → b
}
{ compiling RepeatedCase.g
RepeatedCase.g = λ a → case a of RepeatedCase._,_ b c → b c
}
